$\forall$$A$, $B$:Type, $f$, $g$:($A$$\rightarrow$($B$ + Top)). [$f$?$g$] = p{-}first([$f$; $g$]) $\in$ $A$$\rightarrow$($B$ + Top)